(* Copyright (c) 2016-present, Facebook, Inc.
 *
 * This source code is licensed under the MIT license found in the
 * LICENSE file in the root directory of this source tree. *)

open Core
open Ast
open Pyre
open Assumptions

type class_hierarchy = {
  instantiate_successors_parameters:
    source:Type.t -> target:Type.Primitive.t -> Type.Parameter.t list option;
  is_transitive_successor: source:Type.Primitive.t -> target:Type.Primitive.t -> bool;
  variables: Type.Primitive.t -> Type.Variable.t list option;
  least_upper_bound: Type.Primitive.t -> Type.Primitive.t -> Type.Primitive.t list;
}

type order = {
  class_hierarchy: class_hierarchy;
  all_attributes:
    Type.t -> assumptions:Assumptions.t -> AnnotatedAttribute.instantiated list option;
  attribute:
    Type.t ->
    assumptions:Assumptions.t ->
    name:Ast.Identifier.t ->
    AnnotatedAttribute.instantiated option;
  is_protocol: Type.t -> protocol_assumptions:ProtocolAssumptions.t -> bool;
  get_typed_dictionary: Type.t -> Type.t Type.Record.TypedDictionary.record option;
  metaclass: Type.Primitive.t -> assumptions:Assumptions.t -> Type.t option;
  assumptions: Assumptions.t;
}

module Solution = struct
  (* For now we're just arbitrarily picking the first solution, but we want to allow us the
     opportunity to augment that behavior in the future *)
  include TypeConstraints.Solution
end

type t = TypeConstraints.t list

let empty = [TypeConstraints.empty]

let impossible = []

let potentially_satisfiable constraints_set = List.is_empty constraints_set |> not

type kind =
  | LessOrEqual of {
      left: Type.t;
      right: Type.t;
    }
  | OrderedTypesLessOrEqual of {
      left: Type.OrderedTypes.t;
      right: Type.OrderedTypes.t;
    }
  | VariableIsExactly of Type.Variable.pair

module type OrderedConstraintsSetType = sig
  val add : t -> new_constraint:kind -> order:order -> t

  val solve : ?only_solve_for:Type.Variable.t list -> t -> order:order -> Solution.t option

  val get_parameter_specification_possibilities
    :  t ->
    order:order ->
    parameter_specification:Type.Variable.Variadic.Parameters.t ->
    Type.Callable.parameters list

  val instantiate_protocol_parameters
    :  order ->
    candidate:Type.t ->
    protocol:Ast.Identifier.t ->
    Type.Parameter.t list option
end

let resolve_callable_protocol
    ~assumption
    ~order:{ attribute; assumptions = { callable_assumptions; _ } as assumptions; _ }
    annotation
  =
  match
    CallableAssumptions.find_assumed_callable_type ~candidate:annotation callable_assumptions
  with
  | Some assumption -> Some assumption
  | None -> (
      let new_assumptions =
        {
          assumptions with
          callable_assumptions =
            CallableAssumptions.add ~candidate:annotation ~callable:assumption callable_assumptions;
        }
      in

      attribute annotation ~assumptions:new_assumptions ~name:"__call__"
      >>| AnnotatedAttribute.annotation
      >>| Annotation.annotation
      >>= fun annotation ->
      match annotation with
      | Type.Parametric { name = "BoundMethod"; parameters = [Single _; Single _] }
      | Callable _ ->
          Some annotation
      | _ -> None )


module type OrderedConstraintsType = TypeConstraints.OrderedConstraintsType with type order = order

module Make (OrderedConstraints : OrderedConstraintsType) = struct
  (* TODO(T40105833): merge this with actual signature select *)
  let rec simulate_signature_select
      order
      ~callable:{ Type.Callable.implementation; overloads; _ }
      ~called_as
      ~constraints
    =
    let open Callable in
    let solve implementation ~initial_constraints =
      try
        let rec solve_parameters_against_list_variadic ~is_lower_bound ~concretes ~variable ~tail =
          let before_first_keyword, after_first_keyword_inclusive =
            let is_not_keyword_only = function
              | Type.Callable.Parameter.Keywords _
              | Type.Callable.Parameter.KeywordOnly _ ->
                  false
              | _ -> true
            in
            List.split_while concretes ~f:is_not_keyword_only
          in
          let extract_component = function
            | Type.Callable.Parameter.PositionalOnly { annotation; _ } ->
                Some (Type.OrderedTypes.Concrete [annotation])
            | Named { annotation; _ } when not is_lower_bound ->
                (* Named arguments can be called positionally, but positionals can't be called with
                   a name *)
                Some (Type.OrderedTypes.Concrete [annotation])
            | Variable (Concatenation concatenation) ->
                Some (Type.OrderedTypes.Concatenation concatenation)
            | _ -> None
          in
          let continue =
            if is_lower_bound then
              solve_parameters ~left_parameters:after_first_keyword_inclusive ~right_parameters:tail
            else
              solve_parameters ~left_parameters:tail ~right_parameters:after_first_keyword_inclusive
          in
          let add_bound concretes =
            let left, right =
              if is_lower_bound then
                concretes, variable
              else
                variable, concretes
            in
            solve_ordered_types_less_or_equal order ~left ~right ~constraints
          in
          let concatenate left right =
            left >>= fun left -> Type.OrderedTypes.concatenate ~left ~right
          in
          List.map before_first_keyword ~f:extract_component
          |> Option.all
          >>= List.fold ~init:(Some (Type.OrderedTypes.Concrete [])) ~f:concatenate
          >>| add_bound
          >>| List.concat_map ~f:continue
          |> Option.value ~default:[]
        and solve_parameters ~left_parameters ~right_parameters constraints =
          match left_parameters, right_parameters with
          | Parameter.PositionalOnly _ :: _, Parameter.Named _ :: _ -> []
          | ( Parameter.PositionalOnly { annotation = left_annotation; _ } :: left_parameters,
              Parameter.PositionalOnly { annotation = right_annotation; _ } :: right_parameters )
          | ( Parameter.Named { annotation = left_annotation; _ } :: left_parameters,
              Parameter.PositionalOnly { annotation = right_annotation; _ } :: right_parameters ) ->
              solve_less_or_equal order ~constraints ~left:right_annotation ~right:left_annotation
              |> List.concat_map ~f:(solve_parameters ~left_parameters ~right_parameters)
          | ( Parameter.Variable (Concrete left_annotation) :: left_parameters,
              Parameter.Variable (Concrete right_annotation) :: right_parameters )
          | ( Parameter.Keywords left_annotation :: left_parameters,
              Parameter.Keywords right_annotation :: right_parameters ) ->
              solve_less_or_equal order ~constraints ~left:right_annotation ~right:left_annotation
              |> List.concat_map ~f:(solve_parameters ~left_parameters ~right_parameters)
          | ( Parameter.KeywordOnly ({ annotation = left_annotation; _ } as left) :: left_parameters,
              Parameter.KeywordOnly ({ annotation = right_annotation; _ } as right)
              :: right_parameters )
          | ( Parameter.Named ({ annotation = left_annotation; _ } as left) :: left_parameters,
              Parameter.Named ({ annotation = right_annotation; _ } as right) :: right_parameters )
          | ( Parameter.Named ({ annotation = left_annotation; default = true; _ } as left)
              :: left_parameters,
              Parameter.KeywordOnly ({ annotation = right_annotation; _ } as right)
              :: right_parameters )
          | ( Parameter.Named ({ annotation = left_annotation; default = false; _ } as left)
              :: left_parameters,
              Parameter.KeywordOnly ({ annotation = right_annotation; default = false; _ } as right)
              :: right_parameters ) ->
              if Parameter.names_compatible (Parameter.Named left) (Parameter.Named right) then
                solve_less_or_equal order ~constraints ~left:right_annotation ~right:left_annotation
                |> List.concat_map ~f:(solve_parameters ~left_parameters ~right_parameters)
              else
                impossible
          | ( Parameter.Variable (Concrete left_annotation) :: _,
              Parameter.PositionalOnly { annotation = right_annotation; _ } :: right_parameters ) ->
              solve_less_or_equal order ~constraints ~left:right_annotation ~right:left_annotation
              |> List.concat_map ~f:(solve_parameters ~left_parameters ~right_parameters)
          | ( Parameter.Variable (Concatenation left_variable) :: left_parameters,
              Parameter.Variable (Concatenation right_variable) :: right_parameters ) ->
              solve_ordered_types_less_or_equal
                order
                ~left:(Type.OrderedTypes.Concatenation left_variable)
                ~right:(Type.OrderedTypes.Concatenation right_variable)
                ~constraints
              |> List.concat_map ~f:(solve_parameters ~left_parameters ~right_parameters)
          | left, Parameter.Variable (Concatenation right_variable) :: right_parameters ->
              solve_parameters_against_list_variadic
                ~is_lower_bound:false
                ~concretes:left
                ~variable:(Concatenation right_variable)
                ~tail:right_parameters
          | Parameter.Variable (Concatenation left_variable) :: left_parameters, right ->
              solve_parameters_against_list_variadic
                ~is_lower_bound:true
                ~concretes:right
                ~variable:(Concatenation left_variable)
                ~tail:left_parameters
          | ( Parameter.Variable (Concrete variable_annotation)
              :: Parameter.Keywords keywords_annotation :: _,
              Parameter.Named { annotation = named_annotation; _ } :: right_parameters ) ->
              if Type.equal variable_annotation keywords_annotation then
                solve_less_or_equal
                  order
                  ~constraints
                  ~left:named_annotation
                  ~right:keywords_annotation
                |> List.concat_map ~f:(solve_parameters ~left_parameters ~right_parameters)
              else
                impossible
          | Parameter.Variable _ :: left_parameters, right_parameters
          | Parameter.Keywords _ :: left_parameters, right_parameters ->
              solve_parameters ~left_parameters ~right_parameters constraints
          | left :: left_parameters, [] ->
              if Parameter.default left then
                solve_parameters ~left_parameters ~right_parameters:[] constraints
              else
                impossible
          | [], [] -> [constraints]
          | _ -> impossible
        in
        match implementation.parameters, called_as.parameters with
        | Undefined, Undefined -> [initial_constraints]
        | Defined implementation, Defined called_as ->
            solve_parameters
              ~left_parameters:implementation
              ~right_parameters:called_as
              initial_constraints
        (* We exhibit unsound behavior when a concrete callable is passed into one expecting a
           Callable[..., T] - Callable[..., T] admits any parameters, which is not true when a
           callable that doesn't admit kwargs and varargs is passed in. We need this since there is
           no good way of representing "leave the parameters alone and change the return type" in
           the Python type system at the moment. *)
        | Defined _, Undefined -> [initial_constraints]
        | Undefined, Defined _ -> [initial_constraints]
        | bound, ParameterVariadicTypeVariable { head = []; variable }
          when Type.Variable.Variadic.Parameters.is_free variable ->
            let pair = Type.Variable.ParameterVariadicPair (variable, bound) in
            OrderedConstraints.add_upper_bound initial_constraints ~order ~pair |> Option.to_list
        | bound, ParameterVariadicTypeVariable { head; variable }
          when Type.Variable.Variadic.Parameters.is_free variable ->
            let constraints, remainder =
              match bound with
              | Undefined -> [initial_constraints], Undefined
              | ParameterVariadicTypeVariable { head = left_head; variable = left_variable } ->
                  let paired, remainder = List.split_n left_head (List.length head) in
                  ( solve_ordered_types_less_or_equal
                      order
                      ~left:(Concrete paired)
                      ~right:(Concrete head)
                      ~constraints:initial_constraints,
                    ParameterVariadicTypeVariable { head = remainder; variable = left_variable } )
              | Defined defined ->
                  let paired, remainder = List.split_n defined (List.length head) in
                  ( solve_parameters
                      ~left_parameters:paired
                      ~right_parameters:(Type.Callable.prepend_anonymous_parameters ~head ~tail:[])
                      initial_constraints,
                    Defined remainder )
            in
            let pair = Type.Variable.ParameterVariadicPair (variable, remainder) in
            List.filter_map constraints ~f:(OrderedConstraints.add_upper_bound ~order ~pair)
        | ParameterVariadicTypeVariable left, ParameterVariadicTypeVariable right
          when Type.Callable.equal_parameter_variadic_type_variable Type.equal left right ->
            [initial_constraints]
        | _, _ -> impossible
      with
      | _ -> impossible
    in
    let overload_to_instantiated_return_and_altered_constraints overload =
      let namespace = Type.Variable.Namespace.create_fresh () in
      let namespaced_variables =
        Type.Callable { Type.Callable.kind = Anonymous; implementation = overload; overloads = [] }
        |> Type.Variable.all_free_variables
        |> List.map ~f:(Type.Variable.namespace ~namespace)
      in
      let overload =
        map_implementation overload ~f:(Type.Variable.namespace_all_free_variables ~namespace)
      in
      let does_not_leak_namespaced_variables (external_constraints, _) =
        not (TypeConstraints.exists_in_bounds external_constraints ~variables:namespaced_variables)
      in
      let instantiate_return (external_constraints, partial_solution) =
        let instantiated_return =
          TypeConstraints.Solution.instantiate partial_solution overload.annotation
          |> Type.Variable.mark_all_free_variables_as_escaped ~specific:namespaced_variables
        in
        instantiated_return, external_constraints
      in
      solve overload ~initial_constraints:constraints
      |> List.map
           ~f:(OrderedConstraints.extract_partial_solution ~order ~variables:namespaced_variables)
      |> List.concat_map ~f:Option.to_list
      |> List.filter ~f:does_not_leak_namespaced_variables
      |> List.map ~f:instantiate_return
    in
    let overloads =
      if List.is_empty overloads then
        [implementation]
      else if Type.Callable.Overload.is_undefined implementation then
        overloads
      else
        (* TODO(T41195241) always ignore implementation when has overloads. Currently put
           implementation as last resort *)
        overloads @ [implementation]
    in
    List.concat_map overloads ~f:overload_to_instantiated_return_and_altered_constraints


  (* ## solve_less_or_equal, a brief explanation: ##

     At the heart of our handling of generics is this function, solve_less_or_equal.

     This function takes:

     * a statement of the form F(T1, T2, ... Tn) =<= G(T1, T2, ... Tn), where F and G are types
     which may contain any number of free type variables. In this context a free type variable is
     one whose value we are trying to determine. This could be a function level generic, an
     "escaped" type variable from some sort of incomplete initialization, or even some sort of
     synthetic type variable we're using to answer a question like, "if this is an iterable, what
     kind of iterable is it?" for correctly handling *args parameters.

     * a precondition set of constraints (as defined in TypeConstraints.mli) from a previous call to
     solve_less_or_equal (or from somewhere else). This is how you're able to define conjunctions of
     =<= statements, as when you are trying to satisfy a number of argument <-> parameter pairs in
     signature selection

     and returns:

     * an arbitrarily ordered list of constraints (again as defined in Typeconstraints.mli) that
     each are sufficient to satisfy the given statement and the precondition constraints. If this
     list is empty, there is no way to satify those requirements (at least as well as we can know
     that).

     The general strategy undertaken to achieve this behavior is to pairwise recursively break up
     the types in the same way, e.g. we expect to get a tuple on the right if we have a tuple on the
     left, and to handle that by enforcing that each of the contained types be less than their pair
     on the other side (as tuples are covariant). Certain pairs, such as X =<= Union[...] or
     comparing callables with overloads naturally create multiple disjoint possibilities which give
     rise to the list of constraints that we end up returning.

     Once you have enforced all of the statements you would like to ensure are true, you can extract
     possible solutions to the constraints set you have built up with List.filter_map
     ~f:OrderedConstraints.solve *)
  and solve_less_or_equal
      ( {
          class_hierarchy =
            { instantiate_successors_parameters; variables; is_transitive_successor; _ };
          is_protocol;
          assumptions = { protocol_assumptions; _ } as assumptions;
          get_typed_dictionary;
          metaclass;
          _;
        } as order )
      ~constraints
      ~left
      ~right
    =
    let open Type.Record.TypedDictionary in
    let add_fallbacks other =
      Type.Variable.all_free_variables other
      |> List.fold ~init:constraints ~f:OrderedConstraints.add_fallback_to_any
    in
    let solve_less_or_equal_primitives ~source ~target =
      if is_transitive_successor ~source ~target then
        [constraints]
      else if
        is_protocol right ~protocol_assumptions
        && [%compare.equal: Type.Parameter.t list option]
             (instantiate_protocol_parameters order ~candidate:left ~protocol:target)
             (Some [])
      then
        [constraints]
      else
        impossible
    in
    match left, right with
    | _, _ when Type.equal left right -> [constraints]
    | _, Type.Primitive "object" -> [constraints]
    | other, Type.Any -> [add_fallbacks other]
    | _, Type.Top -> [constraints]
    | Type.ParameterVariadicComponent component, _ ->
        let left =
          match Type.Variable.Variadic.Parameters.Components.component component with
          | KeywordArguments ->
              Type.Parametric
                {
                  name = Type.mapping_primitive;
                  parameters = [Single Type.string; Single Type.object_primitive];
                }
          | PositionalArguments -> Type.Tuple (Unbounded Type.object_primitive)
        in
        solve_less_or_equal order ~constraints ~left ~right
    | _, Type.ParameterVariadicComponent _ -> impossible
    | Type.Annotated left, _ -> solve_less_or_equal order ~constraints ~left ~right
    | _, Type.Annotated right -> solve_less_or_equal order ~constraints ~left ~right
    | Type.Any, other -> [add_fallbacks other]
    | Type.Variable left_variable, Type.Variable right_variable
      when Type.Variable.Unary.is_free left_variable && Type.Variable.Unary.is_free right_variable
      ->
        (* Either works because constraining V1 to be less or equal to V2 implies that V2 is greater
           than or equal to V1. Therefore either constraint is sufficient, and we should consider
           both. This approach simplifies things downstream for the constraint solver *)
        let right_greater_than_left, left_less_than_right =
          ( OrderedConstraints.add_lower_bound
              constraints
              ~order
              ~pair:(Type.Variable.UnaryPair (right_variable, left))
            |> Option.to_list,
            OrderedConstraints.add_upper_bound
              constraints
              ~order
              ~pair:(Type.Variable.UnaryPair (left_variable, right))
            |> Option.to_list )
        in
        right_greater_than_left @ left_less_than_right
    | Type.Variable variable, bound when Type.Variable.Unary.is_free variable ->
        let pair = Type.Variable.UnaryPair (variable, bound) in
        OrderedConstraints.add_upper_bound constraints ~order ~pair |> Option.to_list
    | bound, Type.Variable variable when Type.Variable.Unary.is_free variable ->
        let pair = Type.Variable.UnaryPair (variable, bound) in
        OrderedConstraints.add_lower_bound constraints ~order ~pair |> Option.to_list
    | _, Type.Bottom
    | Type.Top, _ ->
        impossible
    | Type.Bottom, _ -> [constraints]
    | _, Type.NoneType -> impossible
    | Type.Callable _, Type.Primitive protocol when is_protocol right ~protocol_assumptions ->
        if
          [%compare.equal: Type.Parameter.t list option]
            (instantiate_protocol_parameters order ~protocol ~candidate:left)
            (Some [])
        then
          [constraints]
        else
          impossible
    | Type.Callable _, Type.Parametric { name; _ } when is_protocol right ~protocol_assumptions ->
        instantiate_protocol_parameters order ~protocol:name ~candidate:left
        >>| Type.parametric name
        >>| (fun left -> solve_less_or_equal order ~constraints ~left ~right)
        |> Option.value ~default:impossible
    | Type.Union lefts, right ->
        solve_ordered_types_less_or_equal
          order
          ~left:(Concrete lefts)
          ~right:(Concrete (List.map lefts ~f:(fun _ -> right)))
          ~constraints
    | Type.NoneType, Type.Union rights when List.exists rights ~f:Type.is_none ->
        (* Technically speaking, removing this special-case still leads to correct, but somewhat
           redundant solutions, when `rights` contains both None and type varaibles *)
        [constraints]
    | Type.NoneType, Type.Union rights ->
        List.concat_map rights ~f:(fun right -> solve_less_or_equal order ~constraints ~left ~right)
    | Type.NoneType, _ -> impossible
    (* We have to consider both the variables' constraint and its full value against the union. *)
    | Type.Variable bound_variable, Type.Union union ->
        solve_less_or_equal
          order
          ~constraints
          ~left:(Type.Variable.Unary.upper_bound bound_variable)
          ~right
        @ List.concat_map
            ~f:(fun right -> solve_less_or_equal order ~constraints ~left ~right)
            union
    | Type.Variable bound_variable, _ ->
        solve_less_or_equal
          order
          ~constraints
          ~left:(Type.Variable.Unary.upper_bound bound_variable)
          ~right
    | _, Type.Variable _bound_variable -> impossible
    | Type.IntExpression _, _
    | _, Type.IntExpression _ ->
        Type.solve_less_or_equal_polynomial
          ~left
          ~right
          ~impossible
          ~solve:(solve_less_or_equal order ~constraints)
    | _, Type.Union rights ->
        if
          Type.Variable.all_variables_are_resolved left
          && Type.Variable.all_variables_are_resolved right
        then
          (* This is a pure performance optimization, but is practically mandatory because there are
             some humongous unions out there *)
          let simple_solve right =
            solve_less_or_equal order ~constraints ~left ~right |> List.is_empty |> not
          in
          if List.exists rights ~f:simple_solve then
            [constraints]
          else
            impossible
        else
          List.concat_map rights ~f:(fun right ->
              solve_less_or_equal order ~constraints ~left ~right)
    | ( Type.Parametric { name = "type"; parameters = [Single left] },
        Type.Parametric { name = "type"; parameters = [Single right] } ) ->
        solve_less_or_equal order ~constraints ~left ~right
    | Type.Parametric { name = "type"; parameters = [Single meta_parameter] }, _ ->
        let through_meta_hierarchy =
          match meta_parameter, right with
          | Primitive meta_parameter, Primitive _ ->
              metaclass meta_parameter ~assumptions
              >>| (fun left -> solve_less_or_equal order ~left ~right ~constraints)
              |> Option.value ~default:impossible
          | _ -> impossible
        in
        let through_protocol_hierarchy =
          match right, is_protocol right ~protocol_assumptions with
          | Primitive right_name, true ->
              if
                [%compare.equal: Type.Parameter.t list option]
                  (instantiate_protocol_parameters order ~candidate:left ~protocol:right_name)
                  (Some [])
              then
                [constraints]
              else
                impossible
          | Parametric { name = right_name; _ }, true ->
              instantiate_protocol_parameters order ~protocol:right_name ~candidate:left
              >>| Type.parametric right_name
              >>| (fun left -> solve_less_or_equal order ~left ~right ~constraints)
              |> Option.value ~default:impossible
          | Callable _, _ -> (
              match meta_parameter with
              | Type.Union types ->
                  solve_less_or_equal
                    order
                    ~constraints
                    ~left:(Type.union (List.map ~f:Type.meta types))
                    ~right
              | _ ->
                  resolve_callable_protocol ~order ~assumption:right left
                  >>| (fun left -> solve_less_or_equal order ~constraints ~left ~right)
                  |> Option.value ~default:impossible )
          | _ -> impossible
        in
        List.append through_protocol_hierarchy through_meta_hierarchy
    | _, Type.Parametric { name = right_name; parameters = right_parameters } ->
        let solve_parameters left_parameters =
          let handle_variables constraints (left, right, variable) =
            match left, right, variable with
            (* TODO kill these special cases *)
            | Type.Parameter.Single Type.Bottom, _, _ ->
                (* T[Bottom] is a subtype of T[_T2], for any _T2 and regardless of its variance. *)
                constraints
            | _, Type.Parameter.Single Type.Top, _ ->
                (* T[_T2] is a subtype of T[Top], for any _T2 and regardless of its variance. *)
                constraints
            | Single Top, _, _ -> impossible
            | ( Single left,
                Single right,
                Type.Variable.Unary { Type.Variable.Unary.variance = Covariant; _ } ) ->
                constraints
                |> List.concat_map ~f:(fun constraints ->
                       solve_less_or_equal order ~constraints ~left ~right)
            | Single left, Single right, Unary { variance = Contravariant; _ } ->
                constraints
                |> List.concat_map ~f:(fun constraints ->
                       solve_less_or_equal order ~constraints ~left:right ~right:left)
            | Single left, Single right, Unary { variance = Invariant; _ } ->
                constraints
                |> List.concat_map ~f:(fun constraints ->
                       solve_less_or_equal order ~constraints ~left ~right)
                |> List.concat_map ~f:(fun constraints ->
                       solve_less_or_equal order ~constraints ~left:right ~right:left)
            | Group left_parameters, Group right_parameters, ListVariadic _ ->
                (* TODO(T47346673): currently all variadics are invariant, revisit this when we add
                   variance *)
                constraints
                |> List.concat_map ~f:(fun constraints ->
                       solve_ordered_types_less_or_equal
                         order
                         ~constraints
                         ~left:left_parameters
                         ~right:right_parameters)
                |> List.concat_map ~f:(fun constraints ->
                       solve_ordered_types_less_or_equal
                         order
                         ~constraints
                         ~left:right_parameters
                         ~right:left_parameters)
            | CallableParameters left, CallableParameters right, ParameterVariadic _ ->
                let left = Type.Callable.create ~parameters:left ~annotation:Type.Any () in
                let right = Type.Callable.create ~parameters:right ~annotation:Type.Any () in
                List.concat_map constraints ~f:(fun constraints ->
                    solve_less_or_equal order ~constraints ~left ~right)
            | _ -> impossible
          in
          variables right_name
          >>= Type.Variable.zip_on_two_parameter_lists ~left_parameters ~right_parameters
          >>| List.fold ~f:handle_variables ~init:[constraints]
        in
        let parameters =
          let parameters = instantiate_successors_parameters ~source:left ~target:right_name in
          match parameters with
          | None when is_protocol right ~protocol_assumptions ->
              instantiate_protocol_parameters order ~protocol:right_name ~candidate:left
          | _ -> parameters
        in
        parameters >>= solve_parameters |> Option.value ~default:impossible
    | Type.Primitive source, Type.Primitive target -> (
        let left_typed_dictionary = get_typed_dictionary left in
        let right_typed_dictionary = get_typed_dictionary right in
        match left_typed_dictionary, right_typed_dictionary with
        | Some { fields = left_fields; _ }, Some { fields = right_fields; _ } ->
            let field_not_found field =
              not
                (List.exists
                   left_fields
                   ~f:([%equal: Type.t Type.Record.TypedDictionary.typed_dictionary_field] field))
            in
            if not (List.exists right_fields ~f:field_not_found) then
              [constraints]
            else
              impossible
        | Some { fields; _ }, None ->
            let left =
              Type.Primitive
                (Type.TypedDictionary.class_name
                   ~total:(Type.TypedDictionary.are_fields_total fields))
            in
            solve_less_or_equal order ~constraints ~left ~right
        | None, Some { fields; _ } ->
            let right =
              Type.Primitive
                (Type.TypedDictionary.class_name
                   ~total:(Type.TypedDictionary.are_fields_total fields))
            in
            solve_less_or_equal order ~constraints ~left ~right
        | None, None -> solve_less_or_equal_primitives ~source ~target )
    | Type.Parametric { name = source; _ }, Type.Primitive target ->
        solve_less_or_equal_primitives ~source ~target
    (* A <= B -> A <= Optional[B].*)
    | Type.Tuple (Type.Unbounded left), Type.Tuple (Type.Unbounded right) ->
        solve_less_or_equal order ~constraints ~left ~right
    | Type.Tuple (Type.Bounded lefts), Type.Tuple (Type.Unbounded right) ->
        let left = Type.OrderedTypes.union_upper_bound lefts in
        solve_less_or_equal order ~constraints ~left ~right
    | Type.Tuple (Type.Bounded left), Type.Tuple (Type.Bounded right) ->
        solve_ordered_types_less_or_equal order ~left ~right ~constraints
    | Type.Tuple (Type.Unbounded parameter), Type.Primitive _ ->
        solve_less_or_equal
          order
          ~constraints
          ~left:(Type.parametric "tuple" [Single parameter])
          ~right
    | Type.Tuple (Type.Bounded (Concrete (_ :: _ as members))), Type.Primitive _ ->
        solve_less_or_equal
          order
          ~constraints
          ~left:(Type.parametric "tuple" [Single (Type.union members)])
          ~right
    | Type.Primitive name, Type.Tuple _ ->
        if Type.Primitive.equal name "tuple" then [constraints] else impossible
    | Type.Tuple _, _
    | _, Type.Tuple _ ->
        impossible
    | ( Type.Callable { Callable.kind = Callable.Named left; _ },
        Type.Callable { Callable.kind = Callable.Named right; _ } ) ->
        if Reference.equal left right then
          [constraints]
        else
          impossible
    | ( Type.Callable
          {
            Callable.kind = Callable.Anonymous;
            implementation = left_implementation;
            overloads = left_overloads;
          },
        Type.Callable
          {
            Callable.kind = Callable.Named _;
            implementation = right_implementation;
            overloads = right_overloads;
          } )
      when Callable.equal_overload Type.equal left_implementation right_implementation
           && List.equal (Callable.equal_overload Type.equal) left_overloads right_overloads ->
        impossible
    | Type.Callable callable, Type.Callable { implementation; overloads; _ } ->
        let fold_overload sofar called_as =
          let call_as_overload constraints =
            simulate_signature_select order ~callable ~called_as ~constraints
            |> List.concat_map ~f:(fun (left, constraints) ->
                   solve_less_or_equal order ~constraints ~left ~right:called_as.annotation)
          in
          List.concat_map sofar ~f:call_as_overload
        in
        List.fold (implementation :: overloads) ~f:fold_overload ~init:[constraints]
    | left, Type.Callable _ ->
        resolve_callable_protocol ~order ~assumption:right left
        >>| (fun left -> solve_less_or_equal order ~constraints ~left ~right)
        |> Option.value ~default:impossible
    | Type.Callable _, _ -> impossible
    | _, Type.Literal _ -> impossible
    | Type.Literal _, _ ->
        solve_less_or_equal order ~constraints ~left:(Type.weaken_literals left) ~right


  and solve_ordered_types_less_or_equal order ~left ~right ~constraints =
    let solve_concrete_against_concrete ~lefts ~rights constraints =
      let folded_constraints =
        let solve_pair constraints left right =
          constraints
          |> List.concat_map ~f:(fun constraints ->
                 solve_less_or_equal order ~constraints ~left ~right)
        in
        List.fold2 ~init:[constraints] ~f:solve_pair lefts rights
      in
      match folded_constraints with
      | List.Or_unequal_lengths.Ok constraints -> constraints
      | List.Or_unequal_lengths.Unequal_lengths -> impossible
    in
    let solve_concrete_against_concatenation ~is_lower_bound ~bound ~concatenation =
      let variable = Type.OrderedTypes.Concatenation.variable concatenation in
      if Type.Variable.Variadic.List.is_free variable then
        let handle_paired paired =
          let left_and_right ~bound ~concatenated =
            if is_lower_bound then bound, concatenated else concatenated, bound
          in
          let middle_vs_concrete ~concrete ~middle constraints =
            let solve constraints =
              match Type.OrderedTypes.Concatenation.Middle.unwrap_if_bare middle with
              | Some variable ->
                  let add_bound =
                    if is_lower_bound then
                      OrderedConstraints.add_lower_bound
                    else
                      OrderedConstraints.add_upper_bound
                  in
                  add_bound
                    constraints
                    ~order
                    ~pair:(Type.Variable.ListVariadicPair (variable, Concrete concrete))
                  |> Option.to_list
              | None ->
                  (* Our strategy for solving Concrete[X0, X1, ... Xn] <: Map[mapper, mapped_var]
                   *   is as follows:
                   * construct n "synthetic" unary type variables
                   * substitute them through the map, generating
                   *   mapper[Synth0], mapper[Synth1], ... mapper[SynthN]
                   * pairwise solve the concrete memebers against the synthetics:
                   *   X0 <: mapper[Synth0] && X1 <: mapper[Synth1] && ... Xn <: Mapper[SynthN]
                   * Solve the resulting constraints to Soln
                   * Add both upper and lower bounds on mapped_var to be
                   *   Soln[Synth0], Soln[Synth1], ... Soln[SynthN]
                   *)
                  let synthetic_variables, synthetic_variable_constraints_set =
                    let namespace = Type.Variable.Namespace.create_fresh () in
                    let synthetic_solve index (synthetics_created_sofar, constraints_set) concrete =
                      let new_synthetic_variable =
                        Type.Variable.Unary.create (Int.to_string index)
                        |> Type.Variable.Unary.namespace ~namespace
                      in
                      let solve_against_concrete constraints =
                        let generated =
                          Type.OrderedTypes.Concatenation.Middle.singleton_replace_variable
                            middle
                            ~replacement:(Type.Variable new_synthetic_variable)
                        in
                        let left, right =
                          if is_lower_bound then
                            concrete, generated
                          else
                            generated, concrete
                        in
                        solve_less_or_equal order ~constraints ~left ~right
                      in
                      ( new_synthetic_variable :: synthetics_created_sofar,
                        List.concat_map constraints_set ~f:solve_against_concrete )
                    in
                    List.foldi concrete ~f:synthetic_solve ~init:(impossible, [constraints])
                  in
                  let consider_synthetic_variable_constraints synthetic_variable_constraints =
                    let instantiate_synthetic_variables solution =
                      List.map
                        synthetic_variables
                        ~f:(TypeConstraints.Solution.instantiate_single_variable solution)
                      |> Option.all
                    in
                    let add_bound concrete =
                      let add_bound ~adder constraints =
                        adder
                          constraints
                          ~order
                          ~pair:(Type.Variable.ListVariadicPair (variable, concrete))
                      in
                      add_bound ~adder:OrderedConstraints.add_lower_bound constraints
                      >>= add_bound ~adder:OrderedConstraints.add_upper_bound
                    in
                    OrderedConstraints.solve ~order synthetic_variable_constraints
                    >>= instantiate_synthetic_variables
                    >>| List.rev
                    >>| (fun substituted -> Type.Record.OrderedTypes.Concrete substituted)
                    >>= add_bound
                  in
                  List.filter_map
                    synthetic_variable_constraints_set
                    ~f:consider_synthetic_variable_constraints
            in
            List.concat_map constraints ~f:solve
          in
          let concrete_vs_concretes constraints ~pairs =
            let solve_pair constraints (concatenated, bound) =
              let left, right = left_and_right ~bound ~concatenated in
              constraints
              |> List.concat_map ~f:(fun constraints ->
                     solve_less_or_equal order ~constraints ~left ~right)
            in
            List.fold ~init:constraints ~f:solve_pair pairs
          in
          let middle, middle_bound = Type.OrderedTypes.Concatenation.middle paired in
          concrete_vs_concretes ~pairs:(Type.OrderedTypes.Concatenation.head paired) [constraints]
          |> middle_vs_concrete ~concrete:middle_bound ~middle
          |> concrete_vs_concretes ~pairs:(Type.OrderedTypes.Concatenation.tail paired)
        in
        Type.OrderedTypes.Concatenation.zip concatenation ~against:bound
        >>| handle_paired
        |> Option.value ~default:impossible
      else
        impossible
    in
    let open Type.OrderedTypes in
    let open Type.Variable.Variadic.List in
    match left, right with
    | left, right when Type.OrderedTypes.equal left right -> [constraints]
    | Any, _
    | _, Any ->
        [constraints]
    | Concatenation concatenation, Concrete bound ->
        solve_concrete_against_concatenation ~is_lower_bound:false ~bound ~concatenation
    | Concrete bound, Concatenation concatenation ->
        solve_concrete_against_concatenation ~is_lower_bound:true ~bound ~concatenation
    | Concrete lefts, Concrete rights -> solve_concrete_against_concrete ~lefts ~rights constraints
    | Concatenation left, Concatenation right -> (
        let unwrap_if_only_variable concatenation =
          Type.OrderedTypes.Concatenation.unwrap_if_only_middle concatenation
          >>= Type.OrderedTypes.Concatenation.Middle.unwrap_if_bare
        in
        match unwrap_if_only_variable left, unwrap_if_only_variable right with
        | Some left_variable, Some right_variable
          when is_free left_variable && is_free right_variable ->
            (* Just as with unaries, we need to consider both possibilities *)
            let right_greater_than_left, left_less_than_right =
              ( OrderedConstraints.add_lower_bound
                  constraints
                  ~order
                  ~pair:(Type.Variable.ListVariadicPair (right_variable, Concatenation left))
                |> Option.to_list,
                OrderedConstraints.add_upper_bound
                  constraints
                  ~order
                  ~pair:(Type.Variable.ListVariadicPair (left_variable, Concatenation right))
                |> Option.to_list )
            in
            right_greater_than_left @ left_less_than_right
        | Some variable, _ when is_free variable ->
            OrderedConstraints.add_upper_bound
              constraints
              ~order
              ~pair:(Type.Variable.ListVariadicPair (variable, Concatenation right))
            |> Option.to_list
        | _, Some variable when is_free variable ->
            OrderedConstraints.add_lower_bound
              constraints
              ~order
              ~pair:(Type.Variable.ListVariadicPair (variable, Concatenation left))
            |> Option.to_list
        | _ -> impossible )


  and instantiate_protocol_parameters
      ( {
          all_attributes;
          attribute;
          class_hierarchy = { variables; _ };
          assumptions = { protocol_assumptions; _ } as assumptions;
          _;
        } as order )
      ~candidate
      ~protocol
      : Type.Parameter.t list option
    =
    match candidate with
    | Type.Primitive candidate_name when Option.is_some (variables candidate_name) ->
        (* If we are given a "stripped" generic, we decline to do structural analysis, as these
           kinds of comparisons only exists for legacy reasons to do nominal comparisons *)
        None
    | Type.Primitive candidate_name when Identifier.equal candidate_name protocol -> Some []
    | Type.Parametric { name; parameters } when Identifier.equal name protocol -> Some parameters
    | _ -> (
        let assumed_protocol_parameters =
          ProtocolAssumptions.find_assumed_protocol_parameters
            protocol_assumptions
            ~candidate
            ~protocol
        in
        match assumed_protocol_parameters with
        | Some result -> Some result
        | None -> (
            let protocol_generics = variables protocol in
            let protocol_generic_parameters =
              protocol_generics
              >>| List.map ~f:(function
                      | Type.Variable.Unary variable ->
                          Type.Parameter.Single (Type.Variable variable)
                      | ListVariadic variable ->
                          Group
                            (Concatenation
                               ( Type.OrderedTypes.Concatenation.Middle.create_bare variable
                               |> Type.OrderedTypes.Concatenation.create ))
                      | ParameterVariadic variable ->
                          CallableParameters (ParameterVariadicTypeVariable { head = []; variable }))
            in
            let new_assumptions =
              ProtocolAssumptions.add
                protocol_assumptions
                ~candidate
                ~protocol
                ~protocol_parameters:(Option.value protocol_generic_parameters ~default:[])
            in
            let assumptions = { assumptions with protocol_assumptions = new_assumptions } in
            let protocol_attributes =
              let is_not_object_or_generic_method attribute =
                let parent = AnnotatedAttribute.parent attribute in
                (not (Type.is_object (Primitive parent)))
                && not (Type.is_generic_primitive (Primitive parent))
              in
              protocol_generic_parameters
              >>| Type.parametric protocol
              |> Option.value ~default:(Type.Primitive protocol)
              |> all_attributes ~assumptions
              >>| List.filter ~f:is_not_object_or_generic_method
            in
            let candidate, desanitize_map =
              match candidate with
              | Type.Callable _ -> candidate, []
              | _ ->
                  (* We don't return constraints for the candidate's free variables, so we must
                     underapproximate and determine conformance in the worst case *)
                  let desanitize_map, sanitized_candidate =
                    let namespace = Type.Variable.Namespace.create_fresh () in
                    let module SanitizeTransform = Type.Transform.Make (struct
                      type state = Type.Variable.pair list

                      let visit_children_before _ _ = true

                      let visit_children_after = false

                      let visit sofar = function
                        | Type.Variable variable when Type.Variable.Unary.is_free variable ->
                            let transformed_variable =
                              Type.Variable.Unary.namespace variable ~namespace
                              |> Type.Variable.Unary.mark_as_bound
                            in
                            {
                              Type.Transform.transformed_annotation =
                                Type.Variable transformed_variable;
                              new_state =
                                Type.Variable.UnaryPair
                                  (transformed_variable, Type.Variable variable)
                                :: sofar;
                            }
                        | transformed_annotation ->
                            { Type.Transform.transformed_annotation; new_state = sofar }
                    end)
                    in
                    SanitizeTransform.visit [] candidate
                  in
                  sanitized_candidate, desanitize_map
            in
            match protocol_attributes with
            | Some all_protocol_attributes ->
                let order_with_new_assumption = { order with assumptions } in
                let attribute_implements constraints_set protocol_attribute =
                  match constraints_set with
                  | [] -> []
                  | _ ->
                      let attribute_annotation attribute =
                        AnnotatedAttribute.annotation attribute |> Annotation.annotation
                      in
                      attribute
                        ~assumptions
                        candidate
                        ~name:(AnnotatedAttribute.name protocol_attribute)
                      >>| attribute_annotation
                      >>| (fun left ->
                            let right =
                              match attribute_annotation protocol_attribute with
                              | Type.Parametric { name = "BoundMethod"; _ } as bound_method ->
                                  attribute ~assumptions bound_method ~name:"__call__"
                                  >>| attribute_annotation
                                  |> Option.value ~default:Type.object_primitive
                              | annotation -> annotation
                            in

                            List.concat_map constraints_set ~f:(fun constraints ->
                                solve_less_or_equal
                                  order_with_new_assumption
                                  ~left
                                  ~right
                                  ~constraints))
                      |> Option.value ~default:[]
                in
                let instantiate_protocol_generics solution =
                  let desanitize =
                    let desanitization_solution = TypeConstraints.Solution.create desanitize_map in
                    let instantiate = function
                      | Type.Parameter.Single single ->
                          Type.Parameter.Single
                            (TypeConstraints.Solution.instantiate desanitization_solution single)
                      | Group group ->
                          Group
                            (TypeConstraints.Solution.instantiate_ordered_types
                               desanitization_solution
                               group)
                      | CallableParameters parameters ->
                          CallableParameters
                            (TypeConstraints.Solution.instantiate_callable_parameters
                               desanitization_solution
                               parameters)
                    in
                    List.map ~f:instantiate
                  in
                  let instantiate = function
                    | Type.Variable.Unary variable ->
                        TypeConstraints.Solution.instantiate_single_variable solution variable
                        |> Option.value ~default:(Type.Variable variable)
                        |> fun instantiated -> Type.Parameter.Single instantiated
                    | ListVariadic variable ->
                        let default =
                          Type.OrderedTypes.Concatenation
                            ( Type.OrderedTypes.Concatenation.Middle.create_bare variable
                            |> Type.OrderedTypes.Concatenation.create )
                        in
                        TypeConstraints.Solution.instantiate_single_list_variadic_variable
                          solution
                          variable
                        |> Option.value ~default
                        |> fun instantiated -> Type.Parameter.Group instantiated
                    | ParameterVariadic variable ->
                        TypeConstraints.Solution.instantiate_single_parameter_variadic
                          solution
                          variable
                        |> Option.value
                             ~default:
                               (Type.Callable.ParameterVariadicTypeVariable { head = []; variable })
                        |> fun instantiated -> Type.Parameter.CallableParameters instantiated
                  in
                  protocol_generics
                  >>| List.map ~f:instantiate
                  >>| desanitize
                  |> Option.value ~default:[]
                in
                List.fold
                  ~init:[TypeConstraints.empty]
                  ~f:attribute_implements
                  all_protocol_attributes
                |> List.filter_map ~f:(OrderedConstraints.solve ~order:order_with_new_assumption)
                |> List.hd
                >>| instantiate_protocol_generics
            | _ -> None ) )


  let add existing_constraints ~new_constraint ~order =
    match new_constraint with
    | LessOrEqual { left; right } ->
        List.concat_map existing_constraints ~f:(fun constraints ->
            solve_less_or_equal order ~constraints ~left ~right)
    | OrderedTypesLessOrEqual { left; right } ->
        List.concat_map existing_constraints ~f:(fun constraints ->
            solve_ordered_types_less_or_equal order ~constraints ~left ~right)
    | VariableIsExactly pair ->
        let add_both_bounds constraints =
          OrderedConstraints.add_upper_bound constraints ~order ~pair
          >>= OrderedConstraints.add_lower_bound ~order ~pair
        in
        List.filter_map existing_constraints ~f:add_both_bounds


  let solve ?only_solve_for constraints_set ~order =
    match only_solve_for with
    | Some variables ->
        let partial_solve constraints =
          OrderedConstraints.extract_partial_solution constraints ~order ~variables >>| snd
        in
        List.find_map constraints_set ~f:partial_solve
    | None -> List.find_map constraints_set ~f:(OrderedConstraints.solve ~order)


  let get_parameter_specification_possibilities constraints_set ~order ~parameter_specification =
    List.filter_map
      constraints_set
      ~f:
        (OrderedConstraints.extract_partial_solution
           ~order
           ~variables:[Type.Variable.ParameterVariadic parameter_specification])
    |> List.map ~f:snd
    |> List.filter_map ~f:(fun solution ->
           TypeConstraints.Solution.instantiate_single_parameter_variadic
             solution
             parameter_specification)
end
